#define   MODAIN
#include "StepByStep.h"

int yyparse(void);

extern FILE *yyin;

#define ADD_PC_FOR_DELETE1

TypedList* TransTypedListToArray(TypedList *Pt, int *Num)
{
  TypedList *Pt1, *Pt2, *Para;
  int        k;

  k = 0;
  for (Pt1 = Pt; Pt1 != NULL; Pt1 = Pt1->next) k++;

  *Num = k;

  Para = Pt1 = (TypedList *) calloc(k, sizeof(TypedList));
  for ( ; Pt != NULL; Pt1++,Pt=Pt2) {
    CopyOneTypedList(Pt1, Pt);

    k = Pt1->VList.ParaIdx;
    if (IsConstant(k)) InsertOneValueIntoValueList(k, &(Pt1->VList));

    Pt2 = Pt->next;  free(Pt);
  }

  return Para;
}

TypedList* CopyTypedList(TypedList *Pt)
{
  TypedList *Pt1, *Pt2, *Pt3;

  Pt1 = NULL;
  while (Pt != NULL) {
    Pt2 = (TypedList *) calloc(1, sizeof(TypedList));
    CopyOneTypedList(Pt2, Pt);

    if (Pt1 == NULL) Pt1 = Pt2;
    else Pt3->next = Pt2;

    Pt3 = Pt2;
    Pt = Pt->next;
  }

  return Pt1;
}

PENode* CopyPENode(PENode *Pt)
{
  PENode *Pt1;
  
  if (Pt == NULL) return NULL;

  Pt1 = (PENode *) calloc(1, sizeof(PENode));
  Pt1->Type = Pt->Type;
  Pt1->Delete = Pt->Delete;
  Pt1->Vars = CopyTypedList(Pt->Vars);
  Pt1->Pred = CopyTokenList(Pt->Pred);
  Pt1->sons = CopyPENode(Pt->sons);
  Pt1->Effect = CopyPENode(Pt->Effect);
  Pt1->next = CopyPENode(Pt->next);

  return Pt1;
}

ActionList* CopyAction(ActionList *Act)
{
  ActionList *Act1;

  if (Act->Effect == NULL) return NULL;
  
  Act1 = (ActionList *) calloc(1, sizeof(ActionList));
  strcpy(Act1->Name, Act->Name);
  strcpy(Act1->Name1, Act->Name1);
  Act1->Type = Act->Type;

  Act1->Para = CopyTypedArray(Act->NumPara, Act->Para);
  Act1->NumPara = Act->NumPara;
  Act1->PC = CopyPENode(Act->PC);
  Act1->Effect = CopyPENode(Act->Effect);
  Act1->next = NULL;

  return Act1;
}

void HandleOrClauseInPC(ActionList *Act)
{
  ActionList *Act1, *Act2;
  PENode     *Pt1, *Pt2, *Pt3;
  char        c1;

  Pt2 = NULL;
  for (Pt3 = Act->PC; Pt3 != NULL; Pt2=Pt3,Pt3=Pt3->next)
    if (Pt3->Type == OR) {
       if (Pt2 == NULL) Act->PC = Pt3->next;
       else Pt2->next = Pt3->next;
       break;
    }

  if (Pt3 == NULL) return;

  Pt1 = Pt3->sons;   free(Pt3);  // Free OR Node

  Act1 = Act;
  for (c1='B',Pt2=Pt1->next; Pt2 != NULL; c1++,Pt2=Pt3) {
    Pt3 = Pt2->next;

    Act2 = CopyAction(Act);
    sprintf(Act2->Name, "%s_%c", Act->Name, c1);

    Pt2->next = Act2->PC;     Act2->PC = Pt2;

    Act2->next = Act1->next;  Act1->next = Act2;
    Act1 = Act2;
  }

  strcat(Act->Name, "_A");
  Pt1->next = Act->PC;    Act->PC = Pt1;
}

int GetPredIndex(char name[])
{
  PredList *Pred;
  int       i;

  if (name[0] == '=') return EQUAL;

  Pred = Predication;
  for (i = 0; i < NumPred; i++,Pred++)
    if (IsSame(name, Pred->Name)) return i;

  return NOFOUND;
}

int GetConstantIndex(char name[])
{
  TypedList *Pt;
  int        i;

  Pt = Constants;
  for (i = 0; i < NumConstant; i++,Pt++)
    if (IsSame(name, Pt->VList.Name)) return CONSTANT+i;

  return NOFOUND;
}

int GetParaIndex(char Name[], int Num, TypedList *Para)
{
  int i;

  if (Name[0] != '?') return GetConstantIndex(Name);

  for (i = 0; i < Num; i++,Para++)
    if (IsSame(Name, Para->VList.Name)) return i;

  return NOFOUND;
}

void TransPEPredList(ActionList *Act, TypedList *Forall, TokenList *Pt)
{
  int idx, idx1;

  Pt->VList.ParaIdx = GetPredIndex(Pt->VList.Name);

  if (Pt->VList.ParaIdx == NOFOUND) {
     printf("\n  Invalid Predication: %s\n\n", Pt->VList.Name);
     exit(ERROR);
  }

  if (IsEqual(Pt->VList.ParaIdx)) Act->Type |= Equal;

  for (Pt = Pt->next; Pt != NULL; Pt = Pt->next) {
    idx = GetParaIndex(Pt->VList.Name, Act->NumPara, Act->Para);

    if (idx == NOFOUND) {
       idx1 = GetParaIndex(Pt->VList.Name, 0, Forall);
       if (idx1 != NOFOUND) idx = FORVAR - idx1;
       else {
              printf("\n  Invalid PCs/Effects of Action: %s\n\n", Act->Name);
              exit(ERROR);
       }
    }

    Pt->VList.ParaIdx = idx;
    if (IsConstant(idx)) InsertOneValueIntoValueList(idx, &(Pt->VList));
  }
}

void TransEffectNode(ActionList *Act, TypedList *Forall, PENode *PE)
{
  for ( ; PE != NULL; PE = PE->next)
    switch (PE->Type) {
      case ATOM:
      case NOT:
           TransPEPredList(Act, Forall, PE->Pred);
           break;
      case OR:
      case AND:
           TransEffectNode(Act, Forall, PE->sons);
           break;
      case WHEN:
           Act->Type |= WHEN;
           TransEffectNode(Act, Forall, PE->sons);	// Condition
           TransEffectNode(Act, Forall, PE->Effect);
           break;
      case FORALL:
           Act->Type |= FORALL;
           TransEffectNode(Act, PE->Vars, PE->sons);
           break;
      case EXIST:
           Act->Type |= EXIST;
           fprintf(Output, "The EXIST Effect of action is error\n");
           exit(ERROR);
      default:
           fprintf(Output, "Invalid Type of Effect\n");
           break;
    }
}

Bool HandleEqualPredition(ActionList *Act)
{
  TokenList *Pt1, *Pt2;
  TypedList *Para;
  PENode    *PE;
  Bool       OK;
  int        N1, N2;

  OK = TRUE;  Para = Act->Para;
  for (PE = Act->PC; OK && PE!=NULL; PE = PE->next)
    if (PE->Type==ATOM && IsEqual(PE->Pred->VList.ParaIdx)) {
       Pt1 = PE->Pred->next;
       Pt2 = Pt1->next;
       N1 = Pt1->VList.ParaIdx;
       N2 = Pt2->VList.ParaIdx;

       if (IsConstant(N2)) {
          if (IsConstant(N1)) OK = (N1 == N2);
          else (Para+N1)->VList.ParaIdx = N2;
       }
       else if (IsConstant(N1)) (Para+N2)->VList.ParaIdx = N1;
    }

  return OK;
}

Bool HandleNotEqualPredition(ActionList *Act)
{
  TokenList *Pt1, *Pt2;
  TypedList *Para;
  PENode    *PE;
  Bool       OK;
  int        N1, N2;

  OK = TRUE;
  Para = Act->Para;
  for (PE = Act->PC; OK && PE != NULL; PE = PE->next)
    if (PE->Type==NOT && IsEqual(PE->Pred->VList.ParaIdx)) {
       Pt1 = PE->Pred->next;
       Pt2 = Pt1->next;
       N1 = Pt1->VList.ParaIdx;
       N2 = Pt2->VList.ParaIdx;

       if (IsConstant(N1) || IsConstant(N2)) OK = (N1 != N2);
       else if ((Para+N1)->VList.Name[0])
               OK = !IsSame((Para+N1)->VList.Name, (Para+N2)->VList.Name);
    }

  return OK;
}

void TransDomainPred(int Num, TypedList *Vars, PENode *PE)
{
  TokenList *Pt;

  if (PE->Type == OR) PE = PE->sons;

  while (PE != NULL) {
    Pt = PE->Pred;
    Pt->VList.ParaIdx = GetPredIndex(Pt->VList.Name);
    if (Pt->VList.ParaIdx == NOFOUND) {
       printf("\n  Invalid Predication(%s) in domain axiom\n\n", Pt->VList.Name);
       exit(ERROR);
    }

    for (Pt = Pt->next; Pt != NULL; Pt = Pt->next)
      Pt->VList.ParaIdx = GetParaIndex(Pt->VList.Name, Num, Vars);

    PE = PE->next;
  }
}

Bool UniformTwoTokens(int Num, int *Para, TokenList *Pt1, TokenList *Pt2)
{
  int i, j;

  while (Pt2 != NULL) {
    i = Pt1->VList.ParaIdx;
    j = Pt2->VList.ParaIdx;

    if (IsConstant(i)) {
       if (i != j) return FALSE;
    }
    else {
           if (Para[i] == NOFOUND) {
              if (!CheckTransform(Num, Para, i, j)) return FALSE;
           }
           else if (Para[i] != j) return FALSE;
        }

    Pt1 = Pt1->next;  Pt2 = Pt2->next;
  }

  return TRUE;
}

PENode *GetSafetyPred(PENode *PE)
{
  SafetyStru *Pt1;
  TokenList  *Pt2, *Pt3;
  PENode     *PE1;
  int         i, Num, *Para;

  for (Pt1 = Safe; Pt1 != NULL; Pt1 = Pt1->next) {
    Num = Pt1->NumPara;
    Para = (int *) calloc(Num, sizeof(int));
    for (i = 0; i < Num; i++) Para[i] = NOFOUND;

    for (PE1 = Pt1->sons; PE1 != NULL; PE1 = PE1->next) {
      Pt2 = PE->Pred;
      Pt3 = PE1->Pred;
      if (Pt2->VList.ParaIdx == Pt3->VList.ParaIdx &&
         UniformTwoTokens(Num, Para, Pt3->next, Pt2->next)) break;
    }

    if (PE1 != NULL) {
       PE1 = PE1->next;
       if (PE1 == NULL) PE1 = Pt1->sons;

       PE1 = CopyPENode(PE1);
       PE1->Type = ATOM;
       for (Pt2 = PE1->Pred->next; Pt2 != NULL; Pt2 = Pt2->next) {
         i = Pt2->VList.ParaIdx;
         if (!IsConstant(i)) Pt2->VList.ParaIdx = Para[i];
       }
       free(Para);

       return PE1;
    }

    free(Para);
  }

  return NULL;
}

#ifdef ADD_PC_FOR_DELETE
void AddPCForDeleteEffect(ActionList *Act)
{
  TokenList *Pt1, *Pt2;
  PENode    *PC, *PE, *PE1;

  for (PE = Act->Effect; PE != NULL; PE = PE->next) {
    if (PE->Type != NOT) continue;

    for (PC = Act->PC; PC != NULL; PC = PC->next) {
      if (PC->Type == NOT) continue;

      Pt1 = PE->Pred;
      Pt2 = PC->Pred;
      while (Pt1 != NULL) {
        if (Pt1->VList.ParaIdx != Pt2->VList.ParaIdx) break;

        Pt1 = Pt1->next;  Pt2 = Pt2->next;
      }

      if (Pt1 == NULL) break;
    }

    if (PC == NULL) {
       PE1 = CopyPENode(PE);
       PE1->Type = ATOM;
       PE1->next = Act->PC;
       Act->PC = PE1;
    }
  }
}
#endif

#ifdef WHEN_CLAUSE
void SplitCondiditionEffect(ActionList *Act)
{
  PENode *PE1, *PE2, *PE3, *PE4;

  PE1 = PE4 = NULL;
  for (PE2 = Act->Effect; PE2 != NULL; PE2 = PE3) {
    PE3 = PE2->next;
    if (PE2->Type != WHEN) PE1 = PE2;
    else {
           if (PE1 == NULL) Act->Effect = PE3;
           else PE1->next = PE3;

           if (PE4 == NULL) Act->CondEffect = PE2;
           else PE4->next = PE2;
           PE4 = PE2;
    }
  }
}
#else
PENode* GetFirstWhenClauseAndDeleteIt(ActionList *Act)
{
  PENode *Pt1, *Pt2;

  Pt1 = NULL;
  for (Pt2 = Act->Effect; Pt2 != NULL; Pt1=Pt2,Pt2=Pt2->next) {
    if (Pt2->Type == WHEN) {
       if (Pt1 == NULL) Act->Effect = Pt2->next;
       else Pt1->next = Pt2->next;

       Pt2->next = NULL;

       return Pt2;
    }
  }

  return NULL;
}

Bool EqualTwoPENodes(PENode *PE1, PENode *PE2)
{
  TokenList *Pt1, *Pt2;

  Pt2 = PE2->Pred;
  for (Pt1 = PE1->Pred; Pt1 != NULL; Pt1 = Pt1->next) {
    if (Pt1->VList.ParaIdx != Pt2->VList.ParaIdx) return FALSE;

    Pt2 = Pt2->next;
  }

  return TRUE;
}

Bool CheckWhenClauseConflict(PENode *PE1, PENode *PE2)
{
  TypeOfNode T1, T2;
  PENode    *PE3;

  for ( ; PE1 != NULL; PE1 = PE1->next) {
    T1 = PE1->Type;
    for (PE3 = PE2; PE3 != NULL; PE3 = PE3->next) {
      T2 = PE3->Type;
      if (((T1==NOT && T2==ATOM) || (T1==ATOM && T2==NOT))
          && EqualTwoPENodes(PE1, PE3)) return TRUE;
    }
  }

  return FALSE;
}

PENode *InsertWhenClauseToAction(PENode *PE1, PENode *PE2)
{
  PENode *PE3, *PE4;

  while (PE1 != NULL) {
    PE3 = PE1->next;

    for (PE4 = PE2; PE4 != NULL; PE4 = PE4->next)
      if (PE4->Type==PE1->Type && EqualTwoPENodes(PE4, PE1)) break;

    if (PE4 != NULL) { FreeTokenList(PE1->Pred);  free(PE1); }
    else { PE1->next = PE2;  PE2 = PE1; }

    PE1 = PE3;
  }

  return PE2;
}

void InsertNotWhenConditionIntoAct(ActionList *Act, PENode *PE)
{
  TypeOfNode Type;
  PENode    *PE1, *PE2;

  if (PE->Type != OR) Type = AND;
  else {
         PE1 = PE;  PE = PE->sons;  free(PE1);
         Type = OR;
  }

  for (PE1 = PE; PE1 != NULL; PE2=PE1,PE1=PE1->next)
    PE1->Type = (PE1->Type==NOT ? ATOM : NOT);

  if (Type==OR || PE==PE2) {
     PE2->next = Act->PC;   Act->PC = PE;
  }
  else {
         PE2 = NewPENode(OR);
         PE2->sons = PE;
         PE2->next = Act->PC;    Act->PC = PE2;
  }
}
#endif

void TranDomainDefine()
{
  DomainAxiom *Pd;
  ActionList  *Act, *Act1;
#ifndef WHEN_CLAUSE
  ActionList  *Act2;
#endif
  SafetyStru  *Pt3;
  PredList    *Pt, *Pt1, *Pt2;
  PENode      *PE1, *PE2, *PE3;
  Bool         OK;
  int          i, k, Num;

  // Translate Constant List into Array
  Constants = TransTypedListToArray(Constants, &NumConstant);
  
  // Translate Predication List into Pred Array
  NumPred = 0;
  for (Pt1 = Predication; Pt1 != NULL; Pt1 = Pt1->next) NumPred++;
  
  Pt1 = Predication;
  Predication = Pt = (PredList *) calloc(NumPred, sizeof(PredList));
  while (Pt1 != NULL) {
    strcpy(Pt->Name, Pt1->Name);
    Pt->Para = TransTypedListToArray(Pt1->Para, &Num);
    Pt->NumPara = Num;

    Pt2 = Pt1->next;  free(Pt1);  Pt1 = Pt2;
    Pt++;
  }

  // Translate Axioms of Domain
  for (Pd = Axioms; Pd != NULL; Pd = Pd->next) {
    Pd->Vars = TransTypedListToArray(Pd->Vars, &k);
    Pd->NumPara = k;
    TransDomainPred(k, Pd->Vars, Pd->Context);
    TransDomainPred(k, Pd->Vars, Pd->Imply);
    k = Pd->Imply->Pred->VList.ParaIdx;
    IsAxiom(k) = TRUE;
  }

  // Translate Safety of Domain
  for (Pt3 = Safe; Pt3 != NULL; Pt3 = Pt3->next) {
    Pt3->Vars = TransTypedListToArray(Pt3->Vars, &Num);
    Pt3->NumPara = Num;

    PE1 = Pt3->sons;
    Pt3->sons = PE1->sons;  free(PE1);
    for (PE1 = Pt3->sons; PE1 != NULL; PE1 = PE1->next) {
      TransDomainPred(Num, Pt3->Vars, PE1);
      IsSafety(PE1->Pred->VList.ParaIdx) = TRUE;
    }
  }

  // Translate Actions
  for (Act1 = Action; Act1 != NULL; Act1 = Act1->next) {
    Act1->Para = TransTypedListToArray(Act1->Para, &Num);
    Act1->NumPara = Num;

    // Transfer PC of Action
    TransEffectNode(Act1, NULL, Act1->PC);

    // Delete Dummy() From Action
    PE2 = NULL;
    for (PE1 = Act1->Effect; PE1 != NULL; PE1 = PE3) {
      PE3 = PE1->next;

      if (PE1->Type!=ATOM || !IsSame(PE1->Pred->VList.Name, DUMMY)) PE2 = PE1;
      else {
             if (PE2 == NULL) Act1->Effect = PE3;
             else PE2->next = PE3;

             FreeTokenList(PE1->Pred);  free(PE1);
      }
    }

    // Transfer Effect of  Action
    TransEffectNode(Act1, NULL, Act1->Effect);
  }

  // Handle When/Or/Axiom Clause and Copy the Effect;
#ifndef WHEN_CLAUSE
  Act2 = NULL;
#endif
  Act = Action;
  while (Act != NULL) {
    HandleOrClauseInPC(Act);

#ifdef WHEN_CLAUSE
    if (IsType(Act->Type, WHEN)) SplitCondiditionEffect(Act);
    Act = Act->next;
#else
    if (!ISTYPE(Act->Type, WHEN)) { Act2 = Act; Act = Act->next; continue; }

    PE1 = GetFirstWhenClauseAndDeleteIt(Act);
    if (PE1 == NULL) {
       Act->Type ^= WHEN;
       Act2 = Act;  Act = Act->next;
       continue;
    }

    if (CheckWhenClauseConflict(PE1->sons, Act->PC) ||
        CheckWhenClauseConflict(PE1->Effect, Act->Effect)) {
        FreePENodeList(PE1);
        if (Act->Effect != NULL) strcat(Act->Name, "0");
        else {
               Act2->next = Act->next;
               FreeOneAction(Act);
               Act = Act2->next;
        }
    }
    else {
           Act1 = CopyAction(Act);
           PE2 = CopyPENode(PE1->sons);
           strcat(Act->Name, "1");

           // Split When Clause into PC and Effect of Action
           // When Clause Structure:
           //      When
           //        |
           //        V
           //       sons   ------> Condition
           //       Effect ------> Effect
           Act->PC = InsertWhenClauseToAction(PE1->sons, Act->PC);
           Act->Effect = InsertWhenClauseToAction(PE1->Effect, Act->Effect);
           free(PE1);

           if (Act1 == NULL) {
              Act2 = Act;
              //Act = Act->next;
           }
           else {
                  InsertNotWhenConditionIntoAct(Act1, PE2);
                  strcat(Act1->Name, "0");
                  Act1->next = Act->next;
                  Act->next = Act1;
           }
    }
#endif
  }

  // Handle Effect and Pred (=)
  k = 0;
  Act = NULL;
  Act1 = Action;
  while (Act1 != NULL) {
    OK = TRUE;
    if (IsType(Act1->Type, Equal)) {
       OK = HandleEqualPredition(Act1);
       if (OK) OK = HandleNotEqualPredition(Act1);
    }

    if (OK) { k++; Act = Act1; Act1 = Act1->next; }
    else {
           if (Act == NULL) Action = Act1->next;
           else Act->next = Act1->next;
           FreeOneAction(Act1);
           if (Act == NULL) Act1 = Action;
           else Act1 = Act->next;
    }
  }
  NumAct = k;

  Act1 = Action;
  Action = Act = (ActionList *) calloc(k, sizeof(ActionList));
  for ( ; Act1 != NULL; Act++,Act1=Act1->next) {
#ifdef ADD_PC_FOR_DELETE
    AddPCForDeleteEffect(Act1);
#endif

    if (Safety)
       for (PE1 = Act1->Effect; PE1 != NULL; PE1 = PE1->next)
         if (PE1->Type==NOT && IsSafety(PE1->Pred->VList.ParaIdx)) {
            PE2 = GetSafetyPred(PE1);
            PE2->next = Act1->PC;
            Act1->PC = PE2;
         }

    PE1 = Act1->PC;
    if (PE1!=NULL && PE1->Type!=ATOM) PE1 = PE1->sons;

    for (Num = 0; PE1 != NULL; PE1 = PE1->next) Num++;
    Act1->NumPC = Num;

    Act->next = Act1;
  }

  if (Axiom) {
     Num = 0;
     for (Pd = Axioms; Pd != NULL; Pd = Pd->next) Num++;

     Action = (ActionList *) realloc(Action,(NumAct+Num)*sizeof(ActionList));

     i = 0;
     Act = Action + NumAct;
     for (Pd = Axioms; Pd != NULL; Act++,Pd=Pd->next) {
       Act1 = (ActionList *) calloc(1, sizeof(ActionList));

       sprintf(Act1->Name, "Axiom_%d", i++);
       strcpy(Act1->Name1, Act1->Name);
       Act1->NumPara = Pd->NumPara;
       Act1->Para = CopyTypedArray(Pd->NumPara, Pd->Vars);
       Act1->PC = CopyPENode(Pd->Context);
       Act1->Effect = CopyPENode(Pd->Imply);

       PE1 = Act1->PC;
       if (PE1!=NULL && PE1->Type!=ATOM) PE1 = PE1->sons;

       for (k = 0; PE1 != NULL; PE1 = PE1->next) k++;
       Act1->NumPC = k;

       Act->next = Act1;
     }

     NumAct += Num;
  }
}

void GetDomainInfo(char *Filename)
{
//char *sup[] = { ":STRIPS", ":EQUALITY",":TYPING", ":ADL",
//                ":DISJUNCTIVE-PRECONDITIONS", ":DOMAIN-AXIOMS",
//                ":CONDITIONAL-EFFECTS",
//                ":EXISTENTIAL-PRECONDITIONS", ":UNIVERSAL-PRECONDITIONS",
//                NULL };
  char *sup[] = { ":Strips", ":Equality",":Typing", ":Adl",
                  ":Disjunctive-Preconditions", ":Domain-Axioms",
                  ":Conditional-Effects",
                  ":Existential-Preconditions", ":Universal-Preconditions",
                  ":Safety-Constraints", NULL };
  StringList *Pt;
  FILE       *File;
  int         i, idx;

  File = fopen(Filename, "r");
  if (File == NULL) {
     printf("No Domain File: %s\n", Filename );
     exit(ERROR);
  }

  lineno = 1; 
  yyin = File;
  yyparse();
  fclose(File);

  // Check domain requirements
  Typing = Axiom = Exist = Universal = Safety = FALSE;

  for (Pt = Require; Pt != NULL; Pt = Pt->next) {
    idx = NOFOUND;
    for (i = 0; sup[i] != NULL; i++)
      if (IsSame(sup[i], Pt->Name)) { idx = i; break; }

    switch (idx) {
      case TYPING:
           Typing = TRUE;
           break;
      case AXIOM:
           Axiom = TRUE;
           break;
      case SAFETY:
           Safety = TRUE;
           break;
      case EXIST_P:
           Exist = TRUE;
           break;
      case UNIVERSAL_P:
           Universal = TRUE;
           break;
      case ADL:
           Exist = Universal = TRUE;
           break;
      case NOFOUND:
           OpsError(NOT_SUPPORTED, Pt->Name);
           yyerror();
           break;
    }
  }
}
